home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 7 / Apprentice-Release7.iso / Environments / Small Eiffel 0.4.8 / lib_show / parking / level.e < prev    next >
Encoding:
Text File  |  1997-04-13  |  1.8 KB  |  107 lines  |  [TEXT/ttxt]
  1. -- Part of SmallEiffel -- Read DISCLAIMER file -- Copyright (C) 
  2. -- Dominique COLNET and Suzanne COLLIN -- colnet@loria.fr
  3. --
  4. class LEVEL
  5.    
  6. creation {ANY}
  7.    make
  8.    
  9. feature {ANY}
  10.    
  11.    count: INTEGER;
  12.      -- Total count of occupied places.
  13.    
  14.    free_count: INTEGER is
  15.       do
  16.      Result := park.count - count;
  17.       end;
  18.    
  19.    capacity : INTEGER is
  20.       do
  21.      Result := count + free_count;
  22.       end;
  23.    
  24.    full: BOOLEAN is
  25.       do
  26.      Result := count = capacity;
  27.       end; 
  28.  
  29. feature {ANY} -- Modifications :
  30.    
  31.    make(max_cars: INTEGER) is
  32.       require
  33.      max_cars > 0;
  34.       do
  35.      !!park.make(1,max_cars);
  36.      !!tickets.make(park.lower,park.upper);
  37.      count := 0;
  38.       ensure
  39.      count = 0;
  40.       end;
  41.    
  42.    arrival(car: INTEGER; arrival_time: DATE) is
  43.       require
  44.      not full;
  45.      car > 0;
  46.       local
  47.      i: INTEGER;
  48.      stop: BOOLEAN;
  49.      ticket: TICKET;
  50.       do
  51.      from  
  52.         i := park.lower;
  53.         stop := false;
  54.      until
  55.         stop
  56.      loop
  57.         if park @ i <= 0 then
  58.            stop := true;
  59.            park.put(car,i);
  60.            !!ticket.make(arrival_time);
  61.            tickets.put(ticket,i);
  62.            count := count + 1;
  63.         end;
  64.         i := i + 1;
  65.      end;
  66.       ensure
  67.      count >= old count + 1;
  68.       end;
  69.    
  70.    departure(car: INTEGER; departure_time: DATE; hour_price: REAL): REAL is
  71.      -- Gives price to pay or -1 when car is not at this level. 
  72.       require
  73.      car > 0;
  74.       local
  75.      i: INTEGER;
  76.       do
  77.      i := park.index_of(car);   
  78.      if (i > park.upper) then
  79.         Result := -1;
  80.      else     
  81.         Result := (tickets @ i).price(departure_time,hour_price);
  82.         tickets.put(Void,i);
  83.         park.put(0,i);
  84.         count := count - 1;
  85.      end;
  86.       end;
  87.    
  88. feature {NONE}
  89.    
  90.    park: ARRAY[INTEGER];
  91.    
  92.    tickets: ARRAY[TICKET];
  93.  
  94. invariant
  95.    
  96.    count >= 0;
  97.    
  98.    free_count >= 0;
  99.    
  100.    capacity = count + free_count;
  101.    
  102.    capacity >= 1;
  103.  
  104.    tickets.count = park.count;
  105.  
  106. end -- class LEVEL
  107.